Better API for extensions changing CSS

Rename the setter to reflect the fact that it's the stylesheet which is
changing

Add a getter to allow some useful checks

diff --git a/js/ui/main.js b/js/ui/main.js
index 1f650fed91779b1c0c6b71f2e0fdcb60835b545d..16f69774e95cf1c9efd08cb445fe439f4ec82b8c 100644 (file)
--- a/js/ui/main.js
+++ b/js/ui/main.js
@@ -208,13 +208,26 @@ function start() {
 }
 
 /**
- * setTheme
+ * getThemeStylesheet:
+ *
+ * Get the theme CSS file that the shell will load
+ *
+ * Returns: A file path that contains the theme CSS,
+ *          null if using the default
+ */
+function getThemeStylesheet()
+{
+    return _css_stylesheet;
+}
+
+/**
+ * setThemeStylesheet:
  * @css_stylesheet: A file path that contains the theme CSS,
  *                  set it to null to use the default
  *
  * Set the theme CSS file that the shell will load
  */
-function setTheme(css_stylesheet)
+function setThemeStylesheet(css_stylesheet)
 {
     _css_stylesheet = css_stylesheet;
 }